$\forall$$k$, $n$:$\mathbb{N}$, $R$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow$Prop). ($\forall$$i$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$. Dec($i$ $R$ $j$)) $\Rightarrow$ ($\forall$$i$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$. Dec($i$ $R$\^{}$k$ $j$))